The invention relates to the generation of a verified algorithm, e.g., an abstraction algorithm, capable of transforming a program, e.g., a protocol and associated correctness properties, from a first form, e.g., concrete or original, to a second form, e.g., abstracted, and more particularly to the generation of such algorithm via an implicit syntax approach to a formal metatheory of programming languages.
As is well known, a system model is a computer program, block of code, or set of program operations that, upon execution, simulates intended properties, i.e., functions and/or features, of a subject system. That is, a system model may represent a system""s protocol and/or specification and its correctness properties, as will be explained. The system model is typically designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. By way of example, it may be useful to create a system model that simulates a communications protocol in order to test the protocol prior to use in a communication system. However, once a system model is created, the model must be verified to determine whether the model accurately simulates the intended properties of the system. This can be accomplished by inputting the model to a model checker. The model checker is a computer program, block of code, or set of program operations that verifies that the performance of the model matches the desired system behavior envisioned by the system designer.
In formal verification, the system model is converted into a finite state machine. As is well known, a finite state machine is a set of states and state transitions which mimic the operation of the system model in response to any given set of system model inputs. More particularly, each state represents a state or operational mode that the system model would enter given a set of inputs, and each transition state indicates the condition, i.e., the value of system model inputs and system model variables, that must be satisfied for the system model to successfully transition from one state to another state.
Once a system model is converted to a state machine, a model checker can test whether the system model operates in accordance with the desired set of expected behaviors, i.e., system properties. In operation, the checker varies the system model inputs and monitors which states the system model enters as a result of the inputs. As will be appreciated by those skilled in the art, this operation is known as searching the state space of the system model. While searching the system model state space, the model checker checks whether the system model enters a state or a cycle of states which the system designers have defined as so-called xe2x80x9cbadxe2x80x9d or unintended operations. Thus, the model checker can identify for the system designers particular problematic system design features that require redesign in order to comply with intended system performance.
However, it is also known that more complicated systems require more complicated system models. This means that the state machine used to represent the system model includes more states and more state transitions, thus, a larger state space. Unfortunately, when the state space becomes larger, it becomes more difficult to determine whether the model is correct. In order to reduce the difficulty in verifying the correctness of such large models, model creators have proposed generating an abstracted version of the model, i.e., a model that represents the actual system but that includes a reduced set of states and transitions. The abstracted system model then serves as input to the model checker. The model checker then has less difficulty in verifying the reduced state program. This abstraction approach requires the creation of an abstraction algorithm (i.e., computer program, block of code, or set of program operations) capable of transforming the original system model into an abstracted system model. However, it must be proven or verified that the abstraction algorithm applies to the model sought to be abstracted. That is, it is critical that the abstraction algorithm be verified for correctness with respect to the protocol or specification to be input thereto.
It is known that theorem proving and model checking can be combined in a useful manner by employing a theorem proving system to verify abstractions of protocols or system specifications, i.e., system models. In particular, as mentioned above, one can often use a model checker to verify some property of a protocol that has an infinite or intractably large state space, by first transforming the original or concrete protocol into a more abstracted version for which model checking is feasible. For example, this is described in: P. Wolper, xe2x80x9cExpressing Interesting Properties of Programs in Propositional Temporal Logic,xe2x80x9d In Proc. 13th Ann. ACM Symp. On Principles of Prog. Lang., January 1986; and E. M. Clarke, O. Grumberg, and D. E. Long, xe2x80x9cModel Checking and Abstraction,xe2x80x9d In Proc. 19th Ann. ACM Symp. on Principles of Prog. Lang., January 1992. A theorem prover can be used to check, for example, that the property (or some transformation of it) holds of the abstract protocol if and only if it holds of the original protocol. This can be done directly by formalizing the two versions of the protocol and proving the specific property of interest. This approach is taken in K. Havelund and N. Shankar, xe2x80x9cExperiments in Theorem Proving and Model Checking for Protocol Verification,xe2x80x9d In Proc. of Formal Methods in Europe (FME), 1996, which discloses using the integration of a BDD (boolean decision diagram) based model checker as a decision procedure in the theorem prover PVS (Prototype Verification System). PVS is disclosed in S. Rajan, N. Shankar, and M. K. Srivas, xe2x80x9cAn Integration of Model Checking with Automated Proof Checking,xe2x80x9d In Proc. of the Seventh International Conference on Computer Aided Verification (CAV ""95), Vol. 939 of Lecture Notes in Computer Science, pages 84-97, Springer-Verlag, 1995.
One can also provide general support for doing this kind of reasoning by formalizing a refinement calculus and methodology relating system specifications and abstractions, as in O. Muller, xe2x80x9cA Verification Environment for I/O Automata Based on Formalized Metatheory,xe2x80x9d PhD thesis, Technische Universitat Munchen, 1998. One can also use a model checker with assumption commitment style reasoning on the abstract system and then use a theorem prover to discharge the assumptions in the concrete system, as in J. Dingel and T. Filkorn, xe2x80x9cModel Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style Reasoning and Theorem Proving,xe2x80x9d In Proc. of the Seventh International Conference on Computer Aided Verification (CAV ""95), Vol. 939 of Lecture Notes in Computer Science, pages 54-69, 1995.
Typically, when a system specification is represented in a theorem prover, a so-called xe2x80x9cshallow embeddingxe2x80x9d is used. In a shallow embedding of a programming or specification language in a theorem prover, programs and specifications are directly interpreted in the logic of the theorem prover. Thus, one formalizes only the semantics of the language. For example, the commands of an imperative programming language might be encoded as objects of type com=statexe2x86x92state, with language constructs for forming commands being operators over this type, for example c1; c2=xcexs:state.c2(c1(s)). Thus, in a shallow embedding, the commands of the imperative language are defined as particular functions of type com, but the type com will also contain objects that are not the meaning of any command expressible in the given programming language.
In comparison to shallow embedding, xe2x80x9cdeep embeddingxe2x80x9d of a programming or specification language includes representing both the semantics and syntax of the embedded formalism in the theorem prover. Using this approach, one might have a type comsyn consisting of abstract syntax trees of commands, and then a meaning function Mxcex5comsynxe2x86x92com. Theorems quantify over syntax trees, and all reasoning about semantics is mediated by M. Deep embeddings are considerably more difficult to reason about in theorem provers. In practice, shallow embeddings are used whenever possible, and deep embeddings are done only when one is interested in some property that cannot be expressed by referring to semantic objects alone. A comparison of these two methods is presented in R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel, xe2x80x9cExperience with Embedding Hardware Description Languages in HOL,xe2x80x9d in International Conference on Theorem Provers in Circuit Design, pages 129-156, North-Holland, 1992. However, many programs or specifications contain properties that cannot be expressed by referring to semantic objects alone and, thus, conventional theorem proving requires the use of deep embeddings.
The concept of representing syntax implicitly in type theory via an inductive predicate is disclosed in R. L. Constable, xe2x80x9cA Note on Complexity Measures for Inductive Classes in Constructive Type Theory,xe2x80x9d Information and Computation, 143(2): 137-153, 1998, where it is proposed as a way of defining internal computational complexity measures. However, no implementations are disclosed and no proofs are given. While the Constable article discusses how to make implicit codes for the syntactic structure of programs explicit, it proposes only using them to reason formally within type theory about the computational complexity of programs. Furthermore, the Constable article does not address the use of implicit syntax together with extraction to synthesize metaprograms.
There is an approach involving program extraction and model checking described in C. Sprenger, xe2x80x9cA Verified Model Checker for the Modal xcexc-Calculus in Coq,xe2x80x9d Proceedings of TACAS98, pages 167-182, 1998, in which the correctness proof of a model checker in the Coq proof checker yields, via extraction, an executable model checker which is then considered as a trusted decision procedure. However, such approach does not employ implicit syntax but rather represents the syntax of the xcexc-calculus using a conventional explicit approach.
Therefore, a need exists for techniques that allow for improved generation of a correctness verified algorithm (e.g., an abstraction algorithm), in conjunction with a theorem proving system, capable of transforming a program (e.g., system model, system protocol, system specification, and its correctness properties) from a first form (e.g., original or concrete) to a second form (e.g., abstracted) that, among other things, is not dependent on deep embeddings and employs unique implicit syntax and program extraction techniques in generating the correctness verified algorithm.
The present invention provides for such improved correctness verification algorithm generation techniques. Such algorithm generation techniques involve an implicit syntax approach to a formal metatheory of programming languages. The techniques of the invention rely on semantic reasoning, which advantageously avoids the complications that arise when formally reasoning about syntax. The semantic reasoning of the invention contains an implicit construction of the result, i.e., the verified algorithm, using inductive predicates over semantic domains that express representability, as will be explained, in a particular protocol language. Advantageously, such implicit construction allows the synthesis of a verified algorithm that transforms an original program into an abstracted version thereof via recursion on syntax.
In a broad aspect of the invention, a method of synthesizing an algorithm for transforming a program from a first form to a second form includes formalizing a language associated with the program to be transformed in accordance with a theorem proving system. Then, the synthesis method includes building a proof in accordance with the theorem proving system based on a theorem asserting a representability associated with the program, the representability being expressed as inductive predicates over semantic domains. Lastly, the algorithm is extracted based on the proof such that the algorithm is capable of transforming the program from the first form to the second form.
In an illustrative embodiment of the invention, we show how to exploit the constructivity of the well-known Nuprl theorem prover, as described in R. L. Constable et al., xe2x80x9cImplementing Mathematics with the Nuprl Proof Development System,xe2x80x9d Prentice-Hall, Englewood Cliffs, N.J., 1986, to synthesize (i.e., generate or create) a particular verified-correct abstraction algorithm. We build a proof in Nuprl from which we can extract a program that then takes a concrete specification (e.g., protocol) as input, tests whether the abstraction method applies to it, and if so, returns the abstracted system specification.
Advantageously, the techniques of the present invention perform such algorithm synthesis without the use a deep embedding. As mentioned, our proof reasons only about semantics, yet we are able to synthesize a program that operates on syntax. That is, we reason only about the semantic aspects of the abstraction method, even though we implicitly are constructing the program that builds abstracted programs.
This implicit construction is based on inductive predicates over semantic domains that express representability in a particular protocol language. As used herein, the term xe2x80x9cinductive predicatexe2x80x9d is a predicate that is defined as the least predicate satisfying some specified closure conditions. The definition of the term xe2x80x9crepresentabilityxe2x80x9d as used herein depends on the protocol language being formalized. A Nuprl definition of representability is given below in section III of the detailed description. For example, we might say that a command cxcex5com is representable if xe2x80x9cthere exist c1, c2xcex5com such that c=c1; c2xe2x80x9d where we will have a disjunct for each kind of command in the language. Viewed constructively, representability takes the place of a type of abstract syntax tree. However, we cannot directly write down a function which takes a command and returns a list of all the program variables occurring in it, since a command is just a function on states that is assumed to be representable, and we cannot in general determine the list of variables from this function. Thus, it is to be understood that representability is a predicate on semantic objects.
By way of further example, representability may be defined for a simplified programming language consisting of only three kinds of commands. A command c (i.e., a member c of com) is representable if: (i) c=skip; or (ii) c:=e (for some variable x and representable expression e); or (iii) c=c1; c2 (where c1 and c2 are representable commands). This exemplary definition also refers to representablity of expressions, which can be analogously defined. This definition has the form of a standard inductive definition.
We illustrate the techniques of the present invention by applying them to a simple but common data abstraction method. The correctness of the abstraction, as well as the representability of the abstract system specification, is proven in Nuprl. We used the program extracted from these proofs to obtain the abstraction of a simple communication protocol.